#ifndef SAT_1TMTCZT7

#define SAT_1TMTCZT7

#include <set>
#include <vector>
#include "Clause.h"

namespace SAT
{
    class Var;
    class SAT
    {
        public:
            SAT ( );
            virtual ~SAT ();

            void evaluerComposante( std::vector< std::set<unsigned int> > &graph, unsigned int c, bool val, std::set<unsigned int> &composanteNonEval, std::vector< std::set<unsigned int> > &tabComp, std::vector<unsigned int> &composanteFC );


            void addClause( Clause c );

            bool solve2Sat( );

            bool is2SatProblem();

            std::vector<Var*>& getVar()
            {
                return _vVar;
            }

            void afficherProbleme()
            {
                std::cerr << "probleme :" << std::endl;
                for (std::set< std::set< std::pair< Var*, bool > > >::iterator it = _Clause._ssData.begin(); it != _Clause._ssData.end(); ++it)
                {
                    for (std::set< std::pair< Var*, bool > >::iterator it2 = it->begin(); it2 != it->end(); ++it2)
                    {
                        if( !it2->second )
                            std::cerr << "!";
                        std::cerr << it2->first << " + ";
                    }
                    std::cerr << std::endl;
                }
                std::cerr << std::endl << std::endl;

            }

        private:
            std::vector<Var*> _vVar;
            std::set<Var*> _sVar;
            Clause _Clause;


    };
}

#endif /* end of include guard: SAT_1TMTCZT7 */
